es, es':ES, P:(es:ESE). es  es' mod es,e.P(es,e)   

latex

Definitions	P  Q, x. t(x), P  Q, A c B, P  Q, Knd, A  B, P & Q, x(s1,s2), es  es' mod es,e.P(es;e), t  T, , x:A. B(x), x(s)
Lemmas	event system wf, es-same-val wf, es-causl wf, iff wf, es-loc wf, subtype rel weakening, subtype rel transitivity, subtype rel set, es-kind wf, IdLnk wf, es-E wf